2023
Conference article
Open Access
Rule-based NLP vs ChatGPT in ambiguity detection, a preliminary study
Fantechi A., Gnesi S., Semini L.
With the rapid advances of AI-based tools, the question of whether to use such tools or conventional rule-based tools often arises in many application domains. In this paper, we address this question when considering the issue of ambiguity in requirements documents. For this purpose, we consider GPT-3 that is the third-generation of the Generative Pretrained Transformer language model, developed by OpenAI and we compare its ambiguity detection capability with that of a publicly available rule-based NLP tool on a few example requirements documents.Source: REFSQ 2023 - 29th International Working Conference on Requirement Engineering: Foundation for Software Quality: Posters and Tools, Barcelona, Spain, 17-20/04/2023
Fantechi A., Gnesi S., Semini L.
With the rapid advances of AI-based tools, the question of whether to use such tools or conventional rule-based tools often arises in many application domains. In this paper, we address this question when considering the issue of ambiguity in requirements documents. For this purpose, we consider GPT-3 that is the third-generation of the Generative Pretrained Transformer language model, developed by OpenAI and we compare its ambiguity detection capability with that of a publicly available rule-based NLP tool on a few example requirements documents.Source: REFSQ 2023 - 29th International Working Conference on Requirement Engineering: Foundation for Software Quality: Posters and Tools, Barcelona, Spain, 17-20/04/2023
See at:
ceur-ws.org 
| ISTI Repository | CNR ExploRA
2022
Journal article
Embargo
VIBE: looking for Variability In amBiguous rEquirements
Fantechi A., Gnesi S., Semini L.
Variability is a characteristic of a software project and describes the fact that a system can be configured in different ways, obtaining different products (variants) from a common code base, accordingly to the software product line paradigm. This paradigm can be conveniently applied in all phases of the software process, starting from the definition and analysis of the requirements. We observe that often requirements contain ambiguities which can reveal an unintentional and implicit source of variability, that has to be detected. To this end we define VIBE, a tool supported process to identify variability aspects in requirements documents. VIBE is defined on the basis of a study of the different sources of ambiguity in natural language requirements documents that are useful to recognize potential variability, and is characterized by the use of a NLP tool customized to detect variability indicators. The tool to be used in VIBE is selected from a number of ambiguity detection tools, after a comparison of their customization features. The validation of VIBE is conducted using real-world requirements documents.Source: The Journal of systems and software 195 (2022). doi:10.1016/j.jss.2022.111540
DOI: 10.1016/j.jss.2022.111540
Metrics:
Fantechi A., Gnesi S., Semini L.
Variability is a characteristic of a software project and describes the fact that a system can be configured in different ways, obtaining different products (variants) from a common code base, accordingly to the software product line paradigm. This paradigm can be conveniently applied in all phases of the software process, starting from the definition and analysis of the requirements. We observe that often requirements contain ambiguities which can reveal an unintentional and implicit source of variability, that has to be detected. To this end we define VIBE, a tool supported process to identify variability aspects in requirements documents. VIBE is defined on the basis of a study of the different sources of ambiguity in natural language requirements documents that are useful to recognize potential variability, and is characterized by the use of a NLP tool customized to detect variability indicators. The tool to be used in VIBE is selected from a number of ambiguity detection tools, after a comparison of their customization features. The validation of VIBE is conducted using real-world requirements documents.Source: The Journal of systems and software 195 (2022). doi:10.1016/j.jss.2022.111540
DOI: 10.1016/j.jss.2022.111540
Metrics:
See at:
Journal of Systems and Software 
| www.sciencedirect.com | CNR ExploRA
2022
Conference article
Restricted
Formal methods for distributed control systems of future railways
Fantechi A., Gnesi S., Haxthausen A. E.
The adoption of formal methods in railway signalling has been the subject of specific tracks of past ISOLA conferences since a decade.Source: ISoLA'22 - 11th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, pp. 243–245, Rhodes, Greece, 22-30/10/2022
DOI: 10.1007/978-3-031-19762-8_19
Metrics:
Fantechi A., Gnesi S., Haxthausen A. E.
The adoption of formal methods in railway signalling has been the subject of specific tracks of past ISOLA conferences since a decade.Source: ISoLA'22 - 11th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, pp. 243–245, Rhodes, Greece, 22-30/10/2022
DOI: 10.1007/978-3-031-19762-8_19
Metrics:
See at:
doi.org | link.springer.com | CNR ExploRA
2021
Conference article
Open Access
Formal analysis of the UNISIG safety application intermediate sub-layer. Applying Formal Methods to railway standard interfaces
Basile D., Fantechi A., Rosadi I.
The combined use of standard interfaces and formal methods is currently under investigation by Shift2Rail, a joint undertaking between railway stakeholders and the EU. Standard interfaces are useful to increase market competition and standardization whilst reducing long-term life cycle costs. Formal methods are needed to achieve interoperability and safety of standard interfaces and are one of the targets of the 4SECURail project funded by Shift2Rail. This paper presents the modelling and analysis of the selected case study of the 4SECURail project: the Safe Application Intermediate sub-layer of the UNISIG RBC/RBC Safe Communication Interface. The adopted formal method is Statistical Model Checking of a network of Stochastic Priced Timed Automata, as provided by the Uppaal SMC tool. The main contributions are: (i) rigorous complete and publicly available models of an official interface specification already in operation, (ii) identification of safety and interoperability issues in the original specification using Statistical Model Checking, (iii) quantification of costs for learning the adopted formal method and developing the carried out analysis.Source: FMICS 2021 - 26th International Conference on Formal Methods for Industrial Critical Systems, pp. 174–190, Online conference, 24-26/08/2021
DOI: 10.1007/978-3-030-85248-1_11
Project(s): 4SECURAIL
Metrics:
Basile D., Fantechi A., Rosadi I.
The combined use of standard interfaces and formal methods is currently under investigation by Shift2Rail, a joint undertaking between railway stakeholders and the EU. Standard interfaces are useful to increase market competition and standardization whilst reducing long-term life cycle costs. Formal methods are needed to achieve interoperability and safety of standard interfaces and are one of the targets of the 4SECURail project funded by Shift2Rail. This paper presents the modelling and analysis of the selected case study of the 4SECURail project: the Safe Application Intermediate sub-layer of the UNISIG RBC/RBC Safe Communication Interface. The adopted formal method is Statistical Model Checking of a network of Stochastic Priced Timed Automata, as provided by the Uppaal SMC tool. The main contributions are: (i) rigorous complete and publicly available models of an official interface specification already in operation, (ii) identification of safety and interoperability issues in the original specification using Statistical Model Checking, (iii) quantification of costs for learning the adopted formal method and developing the carried out analysis.Source: FMICS 2021 - 26th International Conference on Formal Methods for Industrial Critical Systems, pp. 174–190, Online conference, 24-26/08/2021
DOI: 10.1007/978-3-030-85248-1_11
Project(s): 4SECURAIL
Metrics:
See at:
ISTI Repository | link.springer.com | CNR ExploRA
2021
Master thesis
Open Access
Analysing a safe communication protocol in the railway signaling domain with Timed Automata and Statistical Model Checking
Rosadi I.
This thesis focuses on the modeling and the safety requirements verification of a communication system in the railway signaling domain, where the use of standard interfaces and formal methods is increasing and is also expanding at the industrial level.Project(s): 4SECURAIL
Rosadi I.
This thesis focuses on the modeling and the safety requirements verification of a communication system in the railway signaling domain, where the use of standard interfaces and formal methods is increasing and is also expanding at the industrial level.Project(s): 4SECURAIL
See at:
ISTI Repository | sol.unifi.it | CNR ExploRA
2020
Conference article
Open Access
Comparing formal tools for system design: a judgment study
Ferrari A, Mazzantif., Basile D., Ter Beek M. H., Fantechi A.
Formal methods and tools have a long history of successful applications in the design of safety-critical railway products. However, most of the experiences focused on the application of a single method at once, and little work has been performed to compare the applicability of the different available frameworks to the railway context. As a result, companies willing to introduce formal methods in their development process have little guidance on the selection of tools that couldfi t their needs. To address this goal, this paper presents a comparison between 9 different formal tools, namely Atelier B, CADP, FDR4, NuSMV, ProB, Simulink, SPIN, UMC, and UPPAAL SMC. We performed a judgment study, involving 17 experts with experience in formal methods applied to railways. In the study, part of the experts were required to model a railway signaling problem (a moving-block train distancing system) with the different tools, and to provide feedback on their experience. The information produced was then synthesized, and the results were validated by the remaining experts. Based on the outcome of this process, we provide a synthesis that describes when to use a certain tool, and what are the problems that may be faced by modelers. Our experience shows that the different tools serve different purposes, and multiple formal methods are required to fully cover the needs of the railway system design process.Source: ICSE'20 - 42nd International Conference on Software Engineering, pp. 62–74, Seoul, Republic of Korea, 27/6/2020-19/7/2020
DOI: 10.1145/3377811.3380373
Project(s): 4SECURAIL, ASTRail
Metrics:
Ferrari A, Mazzantif., Basile D., Ter Beek M. H., Fantechi A.
Formal methods and tools have a long history of successful applications in the design of safety-critical railway products. However, most of the experiences focused on the application of a single method at once, and little work has been performed to compare the applicability of the different available frameworks to the railway context. As a result, companies willing to introduce formal methods in their development process have little guidance on the selection of tools that couldfi t their needs. To address this goal, this paper presents a comparison between 9 different formal tools, namely Atelier B, CADP, FDR4, NuSMV, ProB, Simulink, SPIN, UMC, and UPPAAL SMC. We performed a judgment study, involving 17 experts with experience in formal methods applied to railways. In the study, part of the experts were required to model a railway signaling problem (a moving-block train distancing system) with the different tools, and to provide feedback on their experience. The information produced was then synthesized, and the results were validated by the remaining experts. Based on the outcome of this process, we provide a synthesis that describes when to use a certain tool, and what are the problems that may be faced by modelers. Our experience shows that the different tools serve different purposes, and multiple formal methods are required to fully cover the needs of the railway system design process.Source: ICSE'20 - 42nd International Conference on Software Engineering, pp. 62–74, Seoul, Republic of Korea, 27/6/2020-19/7/2020
DOI: 10.1145/3377811.3380373
Project(s): 4SECURAIL
, ASTRail Metrics:
See at:
ISTI Repository | 2020.icse-conferences.org | doi.org | CNR ExploRA
2020
Conference article
Open Access
Designing a demonstrator of formal methods for railways infrastructure managers
Basile D., Ter Beek M. H., Fantechi A., Ferrari A., Gnesi S., Masullo L., Mazzanti F., Piattino A., Trentini D.
The Shift2Rail Innovation Programme (IP) is focussing on innovative technologies to enhance the overall railway market segments. Formal methods and standard interfaces have been identified as two key concepts to reduce time-to-market and costs, while ensuring safety, interoperability and standardisation. However, the decision to start using formal methods is still deemed too risky. Demonstrating technical and commercial benefits of both formal methods and standard interfaces is necessary to address the obstacles of learning curve and lack of clear cost/benefit analysis that are hindering their adoption, and this is the goal of the 4SECURail project, recently funded by the Shift2Rail IP. In this paper, we provide the reasoning and the rationale for designing the formal methods demonstrator for the 4SECURail project. The design concerns two important issues that have been analysed: (i) the usefulness of formal methods from the point of view of the infrastructure managers, (ii) the adoption of a semi-formal SysML notation within our formal methods demonstrator process.Source: ISoLA'20 - 9th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation: Applications, pp. 467–485, Rhodes, Greece, 20-30 October, 2020
DOI: 10.1007/978-3-030-61467-6_30
Project(s): 4SECURAIL
Metrics:
Basile D., Ter Beek M. H., Fantechi A., Ferrari A., Gnesi S., Masullo L., Mazzanti F., Piattino A., Trentini D.
The Shift2Rail Innovation Programme (IP) is focussing on innovative technologies to enhance the overall railway market segments. Formal methods and standard interfaces have been identified as two key concepts to reduce time-to-market and costs, while ensuring safety, interoperability and standardisation. However, the decision to start using formal methods is still deemed too risky. Demonstrating technical and commercial benefits of both formal methods and standard interfaces is necessary to address the obstacles of learning curve and lack of clear cost/benefit analysis that are hindering their adoption, and this is the goal of the 4SECURail project, recently funded by the Shift2Rail IP. In this paper, we provide the reasoning and the rationale for designing the formal methods demonstrator for the 4SECURail project. The design concerns two important issues that have been analysed: (i) the usefulness of formal methods from the point of view of the infrastructure managers, (ii) the adoption of a semi-formal SysML notation within our formal methods demonstrator process.Source: ISoLA'20 - 9th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation: Applications, pp. 467–485, Rhodes, Greece, 20-30 October, 2020
DOI: 10.1007/978-3-030-61467-6_30
Project(s): 4SECURAIL
Metrics:
See at:
ISTI Repository | ISTI Repository | link.springer.com | link.springer.com | CNR ExploRA
2020
Conference article
Open Access
30 years of simulation-based quantitative analysis tools: a comparison experiment between Möbius and Uppaal SMC
Basile D., Ter Beek M. H., Di Giandomenico F., Fantechi A., Gnesi S., Spagnolo G. O.
We provide a brief comparison of the modelling and analysis capabilities of two different formalisms and their associated simulation-based tools, acquired from experimenting with these methods and tools on one specific case study. The case study is a cyber-physical system from an industrial railway project, namely a railroad switch heater, and the quantitative properties concern energy consumption and reliability. We modelled and analysed the case study with stochastic activity networks and Möbius on the one hand and with stochastic hybrid automata and Uppaal SMC on the other hand. We give an overview of the performed experiments and highlight specific features of the two methodologies. This yields some pointers for future research and improvements.Source: ISoLA 2020 - 9th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation: Verification Principles, pp. 368–384, Rhodes, Greece, 20-30/10/2020
DOI: 10.1007/978-3-030-61362-4_21
Metrics:
Basile D., Ter Beek M. H., Di Giandomenico F., Fantechi A., Gnesi S., Spagnolo G. O.
We provide a brief comparison of the modelling and analysis capabilities of two different formalisms and their associated simulation-based tools, acquired from experimenting with these methods and tools on one specific case study. The case study is a cyber-physical system from an industrial railway project, namely a railroad switch heater, and the quantitative properties concern energy consumption and reliability. We modelled and analysed the case study with stochastic activity networks and Möbius on the one hand and with stochastic hybrid automata and Uppaal SMC on the other hand. We give an overview of the performed experiments and highlight specific features of the two methodologies. This yields some pointers for future research and improvements.Source: ISoLA 2020 - 9th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation: Verification Principles, pp. 368–384, Rhodes, Greece, 20-30/10/2020
DOI: 10.1007/978-3-030-61362-4_21
Metrics:
See at:
ISTI Repository | doi.org | link.springer.com | CNR ExploRA
2020
Report
Open Access
4SECURail - D.2.1: Specification of formal development demonstrator
Mazzanti F., Basile D., Fantechi A., Gnesi S., Ferrari A., Piattino A., Masullo L., Trentini D.
The overall goal of the Workstream 1 "Demonstrator Development for the use of Formal Methods in Railway Environment", spreading on the activities of Tasks 2.1, 2.2, 2.3 2.4 of the 4SecuRail project is: - the definition of a "formal methods demonstrator process" (shortly Demonstrator) for the rigorous construction and analysis of system specifications (from the point of view of infrastructure managers); - the application of the Demonstrator process to a railway signalling system case study; - with the goal of performing a cost benefits analysis and the evaluation of the required learning curve for the application of this Demonstrator process This Deliverable "Specification of formal development demonstrator", describing the result of the first part of Task 2.1, presents the overall structure of the Demonstrator process and illustrates the selected choices for its architecture, both in terms of methodologies and tools. The specified formal development demonstrator will be experimented with its application to a simple initial case study in the second part of Task 2.1. The experience gained with this initial experimentation will result in the consolidation of the definition of the Demonstrator process prototype (reported in the Deliverable D2.2 of Task 2.1 "Formal development demonstrator prototype - 1st release"). The consolidated process will then be applied in Task 2.3 to the complete case study defined in Task 2.2 and that activity will provide the reference for the costs-benefits analysis of Task 2.4.Source: Project Report, 4SECURail, D2.1, 2020
Project(s): 4SECURAIL
Mazzanti F., Basile D., Fantechi A., Gnesi S., Ferrari A., Piattino A., Masullo L., Trentini D.
The overall goal of the Workstream 1 "Demonstrator Development for the use of Formal Methods in Railway Environment", spreading on the activities of Tasks 2.1, 2.2, 2.3 2.4 of the 4SecuRail project is: - the definition of a "formal methods demonstrator process" (shortly Demonstrator) for the rigorous construction and analysis of system specifications (from the point of view of infrastructure managers); - the application of the Demonstrator process to a railway signalling system case study; - with the goal of performing a cost benefits analysis and the evaluation of the required learning curve for the application of this Demonstrator process This Deliverable "Specification of formal development demonstrator", describing the result of the first part of Task 2.1, presents the overall structure of the Demonstrator process and illustrates the selected choices for its architecture, both in terms of methodologies and tools. The specified formal development demonstrator will be experimented with its application to a simple initial case study in the second part of Task 2.1. The experience gained with this initial experimentation will result in the consolidation of the definition of the Demonstrator process prototype (reported in the Deliverable D2.2 of Task 2.1 "Formal development demonstrator prototype - 1st release"). The consolidated process will then be applied in Task 2.3 to the complete case study defined in Task 2.2 and that activity will provide the reference for the costs-benefits analysis of Task 2.4.Source: Project Report, 4SECURail, D2.1, 2020
Project(s): 4SECURAIL
See at:
ISTI Repository | www.4securail.eu | CNR ExploRA
2020
Conference article
Open Access
Formal Methods for Distributed Computing in Future Railway Systems
Fantechi A., Gnesi S., Haxthausen A. E.
The growingly wide deployment of ERTMS-ETCS systems on high speed lines as well as on freight corridors is already a witness to the possible achievement of high safety standards by means of distributed control algorithms, that span over geographical areas and are able to safely control large physical systems.Source: 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, pp. 389–392, 20-30/10/2020
DOI: 10.1007/978-3-030-61467-6_24
Metrics:
Fantechi A., Gnesi S., Haxthausen A. E.
The growingly wide deployment of ERTMS-ETCS systems on high speed lines as well as on freight corridors is already a witness to the possible achievement of high safety standards by means of distributed control algorithms, that span over geographical areas and are able to safely control large physical systems.Source: 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, pp. 389–392, 20-30/10/2020
DOI: 10.1007/978-3-030-61467-6_24
Metrics:
See at:
backend.orbit.dtu.dk | ISTI Repository | Online Research Database In Technology | link.springer.com | link.springer.com | CNR ExploRA
2020
Conference article
Open Access
An experience with the application of three nlp tools for the analysis of natural language requirements
Arrabito M., Fantechi A., Gnesi S., Semini L.
We report on the experience made with three Natural Language Processing analysis tools, aimed to compare their performance in detecting ambiguity and under-specification in requirements documents, and to compare them with respect to other qualities like learnability, usability, and efficiency. Two industrial tools, Requirements Scout and QVscribe, and an academic one, QuARS, are compared.Source: Quality of Information and Communications Technology 13th International Conference, QUATIC 2020, pp. 488–498, Faro, Portugal, 9-11/09/2020
DOI: 10.1007/978-3-030-58793-2_39
Metrics:
Arrabito M., Fantechi A., Gnesi S., Semini L.
We report on the experience made with three Natural Language Processing analysis tools, aimed to compare their performance in detecting ambiguity and under-specification in requirements documents, and to compare them with respect to other qualities like learnability, usability, and efficiency. Two industrial tools, Requirements Scout and QVscribe, and an academic one, QuARS, are compared.Source: Quality of Information and Communications Technology 13th International Conference, QUATIC 2020, pp. 488–498, Faro, Portugal, 9-11/09/2020
DOI: 10.1007/978-3-030-58793-2_39
Metrics:
See at:
link.springer.com | ISTI Repository | doi.org | CNR ExploRA
2019
Conference article
Open Access
Adopting Formal Methods in an Industrial Setting: The Railways Case
Ter Beek M. H., Boraelv A., Fantechi A., Ferrari A., Gnesi S., Loefving C., Mazzanti F.
The railway sector has seen a large number of successful applications of formal methods and tools. However, up-to-date, structured information about the industrial usage and needs related to formal tools in railways is limited. Two Shift2Rail projects, X2Rail-2 and ASTRail, have addressed this issue by performing a systematic search over the state of the art of formal methods application in railways to identify the best used practices. As part of the work of these projects, questionnaires on formal methods and tools have been designed to gather input and guidance on the adoption of formal methods in the railway domain. Even though the questionnaires were developed independently and distributed to different audiences, the responses show a certain convergence in the replies to the questions common to both. In this paper, we present a detailed report on such convergence, drawing some indications about methods and tools that are considered to constitute the most fruitful approaches to industrial adoption.Source: FM 2019 - Third International Symposium on Formal Methods, pp. 762–772, Porto, Portugal, 7-11 October
DOI: 10.1007/978-3-030-30942-8_46
Project(s): ASTRail
Metrics:
Ter Beek M. H., Boraelv A., Fantechi A., Ferrari A., Gnesi S., Loefving C., Mazzanti F.
The railway sector has seen a large number of successful applications of formal methods and tools. However, up-to-date, structured information about the industrial usage and needs related to formal tools in railways is limited. Two Shift2Rail projects, X2Rail-2 and ASTRail, have addressed this issue by performing a systematic search over the state of the art of formal methods application in railways to identify the best used practices. As part of the work of these projects, questionnaires on formal methods and tools have been designed to gather input and guidance on the adoption of formal methods in the railway domain. Even though the questionnaires were developed independently and distributed to different audiences, the responses show a certain convergence in the replies to the questions common to both. In this paper, we present a detailed report on such convergence, drawing some indications about methods and tools that are considered to constitute the most fruitful approaches to industrial adoption.Source: FM 2019 - Third International Symposium on Formal Methods, pp. 762–772, Porto, Portugal, 7-11 October
DOI: 10.1007/978-3-030-30942-8_46
Project(s): ASTRail
Metrics:
See at:
ISTI Repository | Lecture Notes in Computer Science | link.springer.com | CNR ExploRA
2019
Report
Open Access
ASTrail - Deliverable D4.3 - Validation Report
Ferrari A., Mazzanti F., Basile D., Fantechi A., Gnesi S., Trentini D., Piattino A., Sturani B.
Formal methods are mathematically-based techniques to support the development of software intensive systems. Normally, formal methods oriented to design and verification of systems include (i) a modelling language, which is used to model a system, and (ii) a verification strategy, which is used to verify properties on the system. Formal methods are usually associated to formal tools, which can provide textual or visual editors to create a model of the system, as well as automated verification capabilities. Formal methods have been largely applied in industrial projects, especially in the safety-critical market, including railways. However, it cannot yet be said that a single mature technology has emerged. The Work Package 4 (WP4) of the ASTRail project aims to identify, based on an analysis of the state-of-the- art and on concrete trials, the candidate set of formal and semi-formal methods that appear as the most adequate to be used in the railway context. In the following, when we will use the general term "formal method", we will implicitly include also semi-formal methods, i.e. those methods that use languages for which the semantics is not formally defined but depends on their execution engine. Since formal methods are normally associated with tools, we will also use the terms formal methods and formal tools interchangeably. To address the goal of identifying the most adequate formal methods, WP4 is structured into four tasks (T4.4, in bold, is the focus on the current deliverable): ? Task 4.1 - Benchmarking: this task aims at studying the state-of-the-art and state of the practice of formal and semi-formal methods, by gathering knowledge from the literature and railway practitioners. ? Task 4.2 - Ranking: this task aims at providing a ranking matrix to support the selection of the most adequate formal methods to be used in a certain development context. ? Task 4.3 - Trial Application: this task aims at experimenting the usage of a set of selected formal methods through the modelling of the moving-block system, from Task 2.1. ? Task 4.4 - Validation: this task aims at validating the usage of the selected formal methods by integrating the moving-block model with the automated driving technologies from Task 3.3. The current deliverable D4.3 Validation Report is the output of Task 4.4 - Validation. The results of Task 4.1- 2 and 4.3 have been reported in D4.1 and D4.2 respectively.Source: Project report, ASTRail, Deliverable D4.3, 2019
Project(s): ASTRail
Ferrari A., Mazzanti F., Basile D., Fantechi A., Gnesi S., Trentini D., Piattino A., Sturani B.
Formal methods are mathematically-based techniques to support the development of software intensive systems. Normally, formal methods oriented to design and verification of systems include (i) a modelling language, which is used to model a system, and (ii) a verification strategy, which is used to verify properties on the system. Formal methods are usually associated to formal tools, which can provide textual or visual editors to create a model of the system, as well as automated verification capabilities. Formal methods have been largely applied in industrial projects, especially in the safety-critical market, including railways. However, it cannot yet be said that a single mature technology has emerged. The Work Package 4 (WP4) of the ASTRail project aims to identify, based on an analysis of the state-of-the- art and on concrete trials, the candidate set of formal and semi-formal methods that appear as the most adequate to be used in the railway context. In the following, when we will use the general term "formal method", we will implicitly include also semi-formal methods, i.e. those methods that use languages for which the semantics is not formally defined but depends on their execution engine. Since formal methods are normally associated with tools, we will also use the terms formal methods and formal tools interchangeably. To address the goal of identifying the most adequate formal methods, WP4 is structured into four tasks (T4.4, in bold, is the focus on the current deliverable): ? Task 4.1 - Benchmarking: this task aims at studying the state-of-the-art and state of the practice of formal and semi-formal methods, by gathering knowledge from the literature and railway practitioners. ? Task 4.2 - Ranking: this task aims at providing a ranking matrix to support the selection of the most adequate formal methods to be used in a certain development context. ? Task 4.3 - Trial Application: this task aims at experimenting the usage of a set of selected formal methods through the modelling of the moving-block system, from Task 2.1. ? Task 4.4 - Validation: this task aims at validating the usage of the selected formal methods by integrating the moving-block model with the automated driving technologies from Task 3.3. The current deliverable D4.3 Validation Report is the output of Task 4.4 - Validation. The results of Task 4.1- 2 and 4.3 have been reported in D4.1 and D4.2 respectively.Source: Project report, ASTRail, Deliverable D4.3, 2019
Project(s): ASTRail
See at:
ISTI Repository | www.astrail.eu | CNR ExploRA
2019
Conference article
Open Access
Applying the QARS tool to detect variability
Fantechi A., Gnesi S., Semini L.
In this demo paper we present how to use the QuARS tool to extract variability information from requirements documents. The main functionality of QuARS is to detect ambiguity in Natural Language (NL) requirement documents. Ambiguity in requirements may be due to intentional or unintentional indication of possible variability; an ambiguity detecting tool can hence be useful to analysts and clients to figure the potential of a requirements document to describe a family of different products.Source: SPLC 2019 - 23rd International Systems and Software Product Line Conference, Paris, France, 09-13 September, 2019
DOI: 10.1145/3307630.3342388
Metrics:
Fantechi A., Gnesi S., Semini L.
In this demo paper we present how to use the QuARS tool to extract variability information from requirements documents. The main functionality of QuARS is to detect ambiguity in Natural Language (NL) requirement documents. Ambiguity in requirements may be due to intentional or unintentional indication of possible variability; an ambiguity detecting tool can hence be useful to analysts and clients to figure the potential of a requirements document to describe a family of different products.Source: SPLC 2019 - 23rd International Systems and Software Product Line Conference, Paris, France, 09-13 September, 2019
DOI: 10.1145/3307630.3342388
Metrics:
See at:
ISTI Repository | dl.acm.org | doi.org | CNR ExploRA
2019
Conference article
Open Access
From generic requirements to variability
Fantechi A., Gnesi S., Semini L.
This paper describes a research activity aiming at extracting variability information from ambiguities and vagueness of generic requirement documents, written in Natural Language. The proposed activity continues a research stream focusing on techniques to extract variability information from requirement documents. Here, we study the introduction of a process able to distinguish structural from functional variability, both in the extracted variability model and in the derived lower-level requirements. The problem is stated with reference to an example, a solution proposal is sketched together with related research questions, and a validation path is envisaged.Source: REFSQ-2019 - Workshops, Doctoral Symposium, Live Studies Track, and Poster Track, Essen, Germany, 18 March, 2019.
Fantechi A., Gnesi S., Semini L.
This paper describes a research activity aiming at extracting variability information from ambiguities and vagueness of generic requirement documents, written in Natural Language. The proposed activity continues a research stream focusing on techniques to extract variability information from requirement documents. Here, we study the introduction of a process able to distinguish structural from functional variability, both in the extracted variability model and in the derived lower-level requirements. The problem is stated with reference to an example, a solution proposal is sketched together with related research questions, and a validation path is envisaged.Source: REFSQ-2019 - Workshops, Doctoral Symposium, Live Studies Track, and Poster Track, Essen, Germany, 18 March, 2019.
See at:
ceur-ws.org | ISTI Repository | CNR ExploRA
2018
Journal article
Open Access
Formal methods for the railway sector
Ter Beek M. H., Fantechi A., Ferrari A., Gnesi S., Scopigno R.
Researchers from the Formal Methods and Tools group of ISTI-CNR are working on a review and assessment of the main formal modelling and verification languages and tools used in the railway domain, with the aim of evaluating the actual applicability of the most promising ones to a moving block signalling system model provided by an industrial partner. The research is being conducted in the context of the H2020 Shift2Rail project ASTRail.Source: ERCIM news 112 (2018): 44–45.
Ter Beek M. H., Fantechi A., Ferrari A., Gnesi S., Scopigno R.
Researchers from the Formal Methods and Tools group of ISTI-CNR are working on a review and assessment of the main formal modelling and verification languages and tools used in the railway domain, with the aim of evaluating the actual applicability of the most promising ones to a moving block signalling system model provided by an industrial partner. The research is being conducted in the context of the H2020 Shift2Rail project ASTRail.Source: ERCIM news 112 (2018): 44–45.
See at:
ercim-news.ercim.eu | ISTI Repository | CNR ExploRA
2018
Report
Open Access
ASTRail - Survey on formal methods and tools in railways technical report on the activities performed within ASTRail, Deliverable D4.1
Ferrari A., Ter Beek M. H., Mazzanti F., Basile D., Fantechi A., Gnesi S., Piattino A., Sturani B., Trentini D.
Formal methods have been largely experimented in industry for the development of safety-critical and mission critical products. Despite the quite long story of successful application of formal methods in the railway domain, it cannot yet be said that a single mature technology has emerged. Indeed, any proposed method or technique that goes under the umbrella of formal methods varies in its suitability and applicability to different stages of the signalling system development, and to different subdomains of railway signalling. This Work Package 4 of the ASTRail project aims to identify, on the basis of an analysis of the state of the art, of the past experiences of the involved partners and on work done in previous projects, the candidate set of formal and semi-formal techniques that appear as the most adequate to be used in the different phases of the conception, design and development of a railway equipment in general, and of the class of signalling equipment that is the subject of this project in particular.Source: Project report, ASTRail, Deliverable D4.1, 2018
Project(s): ASTRail
Ferrari A., Ter Beek M. H., Mazzanti F., Basile D., Fantechi A., Gnesi S., Piattino A., Sturani B., Trentini D.
Formal methods have been largely experimented in industry for the development of safety-critical and mission critical products. Despite the quite long story of successful application of formal methods in the railway domain, it cannot yet be said that a single mature technology has emerged. Indeed, any proposed method or technique that goes under the umbrella of formal methods varies in its suitability and applicability to different stages of the signalling system development, and to different subdomains of railway signalling. This Work Package 4 of the ASTRail project aims to identify, on the basis of an analysis of the state of the art, of the past experiences of the involved partners and on work done in previous projects, the candidate set of formal and semi-formal techniques that appear as the most adequate to be used in the different phases of the conception, design and development of a railway equipment in general, and of the class of signalling equipment that is the subject of this project in particular.Source: Project report, ASTRail, Deliverable D4.1, 2018
Project(s): ASTRail
See at:
ISTI Repository | CNR ExploRA
2018
Journal article
Open Access
Detecting requirements defects with NLP patterns: an industrial experience in the railway domain
Ferrari A., Gori G., Rosadini B., Trotta I., Bacherini S., Fantechi A., Gnesi S.
In the railway safety-critical domain requirements documents have to abide to strict quality criteria. Rule-based natural language processing (NLP) techniques have been developed to automatically identify quality defects in natural language requirements. However, the literature is lacking empirical studies on the application of these techniques in industrial settings. Our goal is to investigate to which extent NLP can be practically applied to detect defects in the requirements documents of a railway signalling manufacturer. To address this goal, we first identified a set of typical defects classes, and, for each class, an engineer of the company implemented a set of defect-detection patterns by means of the GATE tool for text processing. After a preliminary analysis, we applied the patterns to a large set of 1866 requirements previously annotated for defects. The output of the patterns was further inspected by two domain experts to check the false positive cases. Additional discard-patterns were defined to automatically remove these cases. Finally, SREE, a tool that searches for typically ambiguous terms, was applied to the requirements. The experiments show that SREE and our patterns may play complementary roles in the detection of requirements defects. This is one of the first works in which defect detection NLP techniques are applied on a very large set of industrial requirements annotated by domain experts. We contribute with a comparison between traditional manual techniques used in industry for requirements analysis, and analysis performed with NLP. Our experience shows that several discrepancies can be observed between the two approaches. The analysis of the discrepancies offers hints to improve the capabilities of NLP techniques with company specific solutions, and suggests that also company practices need to be modified to effectively exploit NLP tools.Source: Empirical software engineering (Print) 23 (2018): 3684–3733. doi:10.1007/s10664-018-9596-7
DOI: 10.1007/s10664-018-9596-7
Project(s): ASTRail
Metrics:
Ferrari A., Gori G., Rosadini B., Trotta I., Bacherini S., Fantechi A., Gnesi S.
In the railway safety-critical domain requirements documents have to abide to strict quality criteria. Rule-based natural language processing (NLP) techniques have been developed to automatically identify quality defects in natural language requirements. However, the literature is lacking empirical studies on the application of these techniques in industrial settings. Our goal is to investigate to which extent NLP can be practically applied to detect defects in the requirements documents of a railway signalling manufacturer. To address this goal, we first identified a set of typical defects classes, and, for each class, an engineer of the company implemented a set of defect-detection patterns by means of the GATE tool for text processing. After a preliminary analysis, we applied the patterns to a large set of 1866 requirements previously annotated for defects. The output of the patterns was further inspected by two domain experts to check the false positive cases. Additional discard-patterns were defined to automatically remove these cases. Finally, SREE, a tool that searches for typically ambiguous terms, was applied to the requirements. The experiments show that SREE and our patterns may play complementary roles in the detection of requirements defects. This is one of the first works in which defect detection NLP techniques are applied on a very large set of industrial requirements annotated by domain experts. We contribute with a comparison between traditional manual techniques used in industry for requirements analysis, and analysis performed with NLP. Our experience shows that several discrepancies can be observed between the two approaches. The analysis of the discrepancies offers hints to improve the capabilities of NLP techniques with company specific solutions, and suggests that also company practices need to be modified to effectively exploit NLP tools.Source: Empirical software engineering (Print) 23 (2018): 3684–3733. doi:10.1007/s10664-018-9596-7
DOI: 10.1007/s10664-018-9596-7
Project(s): ASTRail
Metrics:
See at:
ISTI Repository | Empirical Software Engineering | link.springer.com | CNR ExploRA
2018
Report
Open Access
ASTRail D4.2 - Preliminary Trial Report
Ferrari A., Basile D., Mazzanti F., Fantechi A., Gnesi S., Piattino A., Trentini D.
Formal methods are mathematically-based techniques to support the development of software intensive systems. Normally, formal methods oriented to design and verification of systems include (i) a modelling language, which is used to model a system, and (ii) a verification strategy, which is used to verify properties on the system. Formal methods are usually associated to formal tools, which can provide textual or visual editors to create a model of the system, as well as automated verification capabilities. Formal methods have been largely applied in industrial projects, especially in the safety-critical industry, including railways [BBF18]. However, it cannot yet be said that a single mature technology has emerged. This Work Package 4 (WP4) of the ASTRail project aims to identify, based on an analysis of the state-of- the-art and on concrete trials, the candidate set of formal and semi-formal methods that appear as the most adequate to be used in the railway context. In the following, when we will use the general term "formal method", we will implicitly include also semi-formal methods, i.e., those methods that use languages for which the semantics is not formally defined but depends on their execution engine. Since formal methods are normally associated with tools, we will also use formal methods and formal tools interchangeably. To address the goal of identifying the most adequate formal methods, WP4 is structured into four tasks (T4.3, in bold, is the focus on the current deliverable): - Task 4.1 Benchmarking: this task aims at studying the state-of-the-art and state of the practice of formal and semi-formal methods, by gathering knowledge from the literature and railway practitioners. - Task 4.2 Ranking: this task aims at providing a ranking matrix to support the selection of the most adequate formal methods to be used in a certain development context. - Task 4.3 Trial Application: this task aims at experimenting the usage of a set of selected formal methods through the modelling of the moving-block system, from Task 2.1. - Task 4.4 Validation: this task aims at validating the usage of the selected formal methods by integrating the moving-block model with the automated driving technologies from Task 3.3. The current deliverable, D4.2 Preliminary Trial Report, reports on Task 4.3 Trial Application, while the results of Task 4.1 and 4.2 have been reported in D4.1.Source: Project report, ASTRail, Deliverable D4.2, 2018
Project(s): ASTRail
Ferrari A., Basile D., Mazzanti F., Fantechi A., Gnesi S., Piattino A., Trentini D.
Formal methods are mathematically-based techniques to support the development of software intensive systems. Normally, formal methods oriented to design and verification of systems include (i) a modelling language, which is used to model a system, and (ii) a verification strategy, which is used to verify properties on the system. Formal methods are usually associated to formal tools, which can provide textual or visual editors to create a model of the system, as well as automated verification capabilities. Formal methods have been largely applied in industrial projects, especially in the safety-critical industry, including railways [BBF18]. However, it cannot yet be said that a single mature technology has emerged. This Work Package 4 (WP4) of the ASTRail project aims to identify, based on an analysis of the state-of- the-art and on concrete trials, the candidate set of formal and semi-formal methods that appear as the most adequate to be used in the railway context. In the following, when we will use the general term "formal method", we will implicitly include also semi-formal methods, i.e., those methods that use languages for which the semantics is not formally defined but depends on their execution engine. Since formal methods are normally associated with tools, we will also use formal methods and formal tools interchangeably. To address the goal of identifying the most adequate formal methods, WP4 is structured into four tasks (T4.3, in bold, is the focus on the current deliverable): - Task 4.1 Benchmarking: this task aims at studying the state-of-the-art and state of the practice of formal and semi-formal methods, by gathering knowledge from the literature and railway practitioners. - Task 4.2 Ranking: this task aims at providing a ranking matrix to support the selection of the most adequate formal methods to be used in a certain development context. - Task 4.3 Trial Application: this task aims at experimenting the usage of a set of selected formal methods through the modelling of the moving-block system, from Task 2.1. - Task 4.4 Validation: this task aims at validating the usage of the selected formal methods by integrating the moving-block model with the automated driving technologies from Task 3.3. The current deliverable, D4.2 Preliminary Trial Report, reports on Task 4.3 Trial Application, while the results of Task 4.1 and 4.2 have been reported in D4.1.Source: Project report, ASTRail, Deliverable D4.2, 2018
Project(s): ASTRail
See at:
ISTI Repository | www.astrail.eu | CNR ExploRA
2018
Contribution to book
Open Access
Applications of formal methods, modeling, and testing strategies for safe software development
Fantechi A., Ferrari A., Gnesi S.
The challenges posed by the new scenarios of railway transportation (liberalization, dis- tinction between infrastructure and operation, high speed, European interoperability, etc.) have a dramatic impact on the safety issues. This impact is counterbalanced by the grow- ing adoption of innovative signaling equipment (the most notable example is the European Rail Traffic Management System/European Train Control System) and monitoring sys- tems (such as onboard and wayside diagnosis systems). Each one of these devices includes some software, which in the end makes up the major part of their design costs; the malle- ability of the software is paramount for the innovation of solutions. On the other hand, it is notorious how software is often plagued by bugs that may threaten its correct functioning: how can the high safety standards assumed as normal practice in railway operation be compatible with such threats?Source: Handbook of RAMS in Railway Systems, edited by Qamar Mahboob, Enrico Zio, pp. 275–295, 2018
Project(s): ASTRail
Fantechi A., Ferrari A., Gnesi S.
The challenges posed by the new scenarios of railway transportation (liberalization, dis- tinction between infrastructure and operation, high speed, European interoperability, etc.) have a dramatic impact on the safety issues. This impact is counterbalanced by the grow- ing adoption of innovative signaling equipment (the most notable example is the European Rail Traffic Management System/European Train Control System) and monitoring sys- tems (such as onboard and wayside diagnosis systems). Each one of these devices includes some software, which in the end makes up the major part of their design costs; the malle- ability of the software is paramount for the innovation of solutions. On the other hand, it is notorious how software is often plagued by bugs that may threaten its correct functioning: how can the high safety standards assumed as normal practice in railway operation be compatible with such threats?Source: Handbook of RAMS in Railway Systems, edited by Qamar Mahboob, Enrico Zio, pp. 275–295, 2018
Project(s): ASTRail
See at:
ISTI Repository | www.taylorfrancis.com | CNR ExploRA